\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+
\\[0ex]${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$).
\-\\[0ex]update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ fpf{-}compatible(\=Knd;\+
\\[0ex]$k$.Type;
\\[0ex]Kind{-}deq;
\\[0ex]R{-}da(ecl{-}machine\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$); $i$);
\\[0ex]${\it da}$)
\-
\end{tabbing}